r,s:rationals. (qpositive(r))  (qpositive(s))  (qpositive((r + s))) 

latex

Definitions	guard(T), gt(i; j), prop{i:l}, P  Q, P  Q, ff, tt, qinv(r), r * s, if b then t else f fi , t  T, qdiv(r; s), r + s, qpositive(r), P  Q, x:A. B(x), False, A, nequal(T; a; b), P  Q, P  Q, A c B, int_nzero, x:A. B(x)
Lemmas	gt wf, neg mul arg bounds, pos mul arg bounds, rationals wf, qadd wf, qpositive wf, assert of lt int, and functionality wrt iff, assert of band, or functionality wrt iff, assert of bor, iff transitivity, lt int wf, band wf, bor wf, assert wf, implies functionality wrt iff, int nzero properties, q-elim